\begin{tabbing}
es{-}frame(${\it es}$;$i$;$L$;$x$;$T$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}vartype(${\it es}$; $i$; $x$) $\subseteq\rho$ $T$\+
\\[0ex]\& alle{-}at(${\it es}$;$i$;$e$.\=$\neg$(es{-}kind(${\it es}$; $e$) $\in$ $L$ $\in$ Knd)\+
\\[0ex]$\Rightarrow$ es{-}after(${\it es}$; $x$; $e$) $=$ es{-}when(${\it es}$; $x$; $e$) $\in$ $T$)
\-\-
\end{tabbing}